/* Franco, 19/03/2010

   Main file for testing "deep" models. Take one parameter, the depth
   of the model

*/

#include "cuddObj.hh"
#include "utilities.hh"
#include "formula.hh"
#include <cmath>
// #include <ctime>



int main(int argc, char* argv[]) {

  // Initial declarations, valid for all models
  clock_t begin=clock();
  Cudd *bddmgr = new Cudd(0,0);
  map<string, BDD*> *evaluation = new map<string,BDD*>();
  BDD *Rt = new BDD();
  BDD *Ri = new BDD();
  vector<BDD *> *EC = new vector<BDD *>();
  int depth = 0; // the max depth of a computation (see reachable
		 // states)


  Cudd_ReorderingType REORDERING = CUDD_REORDER_GROUP_SIFT_CONV;
  Cudd_AutodynEnable(bddmgr->getManager(), REORDERING);

  // Model-specific code
  int states_count = atoi(argv[1]); 
  states_count = states_count + 1;
  cout << "  N. bits: " << states_count << endl;
  BDDvector *v = new BDDvector(states_count,bddmgr); 
  BDDvector *pv = new BDDvector(states_count,bddmgr); 
  
  for (int i = 0; i < states_count; i++) {
    (*v)[i] = bddmgr->bddVar(i);
    (*pv)[i] = bddmgr->bddVar(states_count + i);
  }  

  build_deep_model(states_count-1,bddmgr,v,pv,Rt,Ri,evaluation);  
  // End of model specific code


  // Compute reachable (assuming state 0 is the initial state)
  BDD *reach = new BDD();
  //  cout << "Computing the set of reachable states..." << endl;
  reach = compute_reachable_states(stateid_to_BDD(0,v,bddmgr),Rt,v,
				   pv,bddmgr,depth);
  //  cout << "Reachable states done" << endl;

  //  cout << "Computing equivalence classes..." << endl;
  // Compute equivalence classes
  EC = compute_EC(Ri,v,pv,bddmgr,reach);
  //  cout << "Equivalence classes done" << endl;

  // MODEL CHECKING PART

  BDD *result = new BDD();

  Formula* atom_a = new Formula("a");

  //  cout << "Now playing with K1" << endl;
  Formula* k1a = new Formula(32,atom_a);
  k1a->set_depth(1);
  k1a->set_EC(EC);

  clock_t f1begin=clock();
  result = (k1a->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
			       reach));
  clock_t f1end=clock();
  cout << "    f1 time: " <<diffclock(f1end,f1begin)<<" ms" << endl;
  //  result->print(2,2);


  //  cout << "Now playing with KPR" << endl;

  Formula* kpra = new Formula(31,atom_a);
  kpra->set_model_depth(depth);
  kpra->set_EC(EC);
  clock_t f2begin=clock();
  result = (kpra->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
			       reach));
  //  result->print(2,2);
  clock_t f2end=clock();
  cout << "    f2 time: " <<diffclock(f2end,f2begin)<<" ms" << endl;


  Formula* k10pra = new Formula(31,atom_a);
  k10pra->set_model_depth(depth);
  k10pra->set_EC(EC);
  Formula* k11pra = new Formula(31,k10pra);
  k11pra->set_model_depth(depth);
  k11pra->set_EC(EC);
  Formula* k12pra = new Formula(31,k11pra);
  k12pra->set_model_depth(depth);
  k12pra->set_EC(EC);
  Formula* k13pra = new Formula(31,k12pra);
  k13pra->set_model_depth(depth);
  k13pra->set_EC(EC);
  Formula* k14pra = new Formula(31,k13pra);
  k14pra->set_model_depth(depth);
  k14pra->set_EC(EC);
  Formula* k15pra = new Formula(31,k14pra);
  k15pra->set_model_depth(depth);
  k15pra->set_EC(EC);
  Formula* k16pra = new Formula(31,k15pra);
  k16pra->set_model_depth(depth);
  k16pra->set_EC(EC);
  Formula* k17pra = new Formula(31,k16pra);
  k17pra->set_model_depth(depth);
  k17pra->set_EC(EC);
  Formula* k18pra = new Formula(31,k17pra);
  k18pra->set_model_depth(depth);
  k18pra->set_EC(EC);
  Formula* k19pra = new Formula(31,k18pra);
  k19pra->set_model_depth(depth);
  k19pra->set_EC(EC);
  Formula* k20pra = new Formula(31,k19pra);
  k20pra->set_model_depth(depth);
  k20pra->set_EC(EC);
  clock_t f3begin=clock();
  result = (k20pra->check_formula(v,pv,Rt,Ri,bddmgr,evaluation,
			       reach));
  //  result->print(2,2);
  clock_t f3end=clock();
  cout << "    f3 time: " <<diffclock(f3end,f3begin)<<" ms" << endl;


  clock_t end=clock();
  cout << "  Total time: " <<diffclock(end,begin)<<" ms" << endl;

}
